T:Type, P:(T), L2, L1:(T List). fseg(T;L1;L2)  fseg(T;filter(P;L1);filter(P;L2)) 

latex

ProofTree

Definitions	s ~ t, x:AB(x), x:A. B(x), as @ bs, type List, s = t, Type, x:A  B(x), x:A. B(x), , t  T, {x:A| B(x)} , , {T}, P  Q, SQType(T), , [car / cdr], P & Q, P  Q, P  Q, A  B, i  j , ||as||, fseg(T;L1;L2), filter(P;l)
Lemmas	bool wf, fseg wf, non neg length, cons one one, guard wf, nat wf, member wf, filter append